Replace dependency on domain_shims with lightweight DLS shim for single-threaded OCaml
#186
Conversation
michael-schwarz
changed the title
domain_shims with lightweight DLS shim for single-threaded OCamldomain_shims with lightweight DLS shim for single-threaded OCaml
There was a problem hiding this comment.
Besides the clear race condition, I think doing it like this in CIL won't really fix the problem. For the same reason like our Zarith patch: it needs to be fork and pin of the original package, not in a new package, because other things we depend on would probably still use the original domain_shims.
I think we should just remove the global state from Pretty and be done with it. There's no reason it shouldn't be possible and there's every reason to have less global state anyway.
| let v = k.initialiser () in | ||
| k.value <- Some v; |
There was a problem hiding this comment.
I'm not sure this really works. There's a race condition here (yes, on OCaml 4 without threads!):
If the signal handler fires between these two lines to set something, then this get (!) will overwrite the "new" value with the initial one.
There's a good reason why domain_shims uses atomicity (although via a Dirk-style mutex). I think atomicity is inevitable in a correct solution: it's just that the atomicity probably should be proper, not using a mutex, possibly with a lock-free data structure.
It is not a general fix of the problem in This is a fix to get back pre-DLS behavior from OCaml 4. Yes, the usage in Goblint is problematic, but it has been problematic all along, and this solution is no less problematic then the old solution using
If you want to commit resources to this within the next few days, sure. Otherwise, I think this is a good stop-gap until someone invests the time in such a re-write of Pretty (it has more state than just these few things btw). |
It was 30 min of straightforward work: PR #187. |
|
Closing in favor of #187. It is the more principled approach. |
Instead of using the
domain_shimslibrary to simulate all aspects of domains, this provides just a shim for DLS as we don't use multiple domains for OCaml 4 anyway.This fixes goblint/analyzer#1781 without any principled rework.